M:MsgA. M || M 

latex

Definitions	M1 || M2, MsgA, M1 ||decl M2, f || g, IdLnkDeq, product-deq(A;B;a;b), f  g, Valtype(da;k), Prop, locl(a), State(ds), 1of(t), f(x)?z, EqDecider(T), x(s), T, True, rcv(l,tg), 2of(t), IdLnk, IdDeq, KindDeq, P  Q, P & Q, P  Q, Knd, x. t(x), P  Q, strong-subtype(A;B), x:A. B(x), Id, Top, a:A fp B(a), t  T
Lemmas	strong-subtype-self, subtype-fpf3, fpf wf, Id wf, fpf-join-idempotent, pi2 wf, rcv wf, fpf-cap wf, top wf, ma-state wf, true wf, squash wf, deq wf, pi1 wf, fpf-join wf, ma-valtype wf, locl wf, product-deq wf, idlnk-deq wf, IdLnk wf, Knd wf, Kind-deq wf, id-deq wf, fpf-compatible-self, msga wf